\begin{tabbing}
$\forall$$A$:Type, $I$:MaInterface($A$), $i$:Id.
\\[0ex]($i$ $\in$ ma{-}interface{-}locs($I$))
\\[0ex]$\Rightarrow$ \=($\forall$$k$:Knd.\+
\\[0ex]($k$ $\in$ ma{-}interface{-}dom($I$;$i$))
\\[0ex]$\Rightarrow$ (\=ma{-}interface{-}code($I$;$i$;$k$)\+
\\[0ex]$\in$ State(ma{-}interface{-}ds($I$;$i$))$\rightarrow$ma{-}interface{-}valtype($I$;$i$;$k$)$\rightarrow$($A$ + Top)))
\-\-
\end{tabbing}